/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Scott Morrison
-/
import algebra.module
import data.fintype.card

/-!

# Type of functions with finite support

For any type `α` and a type `β` with zero, we define the type `finsupp α β` of finitely supported
functions from `α` to `β`, i.e. the functions which are zero everywhere on `α` except on a finite
set. We write this in infix notation as `α →₀ β`.

Functions with finite support provide the basis for the following concrete instances:

 * `ℕ →₀ α`: Polynomials (where `α` is a ring)
 * `(σ →₀ ℕ) →₀ α`: Multivariate Polynomials (again `α` is a ring, and `σ` are variable names)
 * `α →₀ ℕ`: Multisets
 * `α →₀ ℤ`: Abelian groups freely generated by `α`
 * `β →₀ α`: Linear combinations over `β` where `α` is the scalar ring

Most of the theory assumes that the range is a commutative monoid. This gives us the big sum
operator as a powerful way to construct `finsupp` elements.

A general piece of advice is to not use `α →₀ β` directly, as the type class setup might not be a
good fit. Defining a copy and selecting the instances that are best suited for the application works
better.

## Implementation notes

This file is a `noncomputable theory` and uses classical logic throughout.

## Notation

This file defines `α →₀ β` as notation for `finsupp α β`.

-/

noncomputable theory
open_locale classical big_operators

open finset

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Type*}
  {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*}

/-- `finsupp α β`, denoted `α →₀ β`, is the type of functions `f : α → β` such that
  `f x = 0` for all but finitely many `x`. -/
structure finsupp (α : Type*) (β : Type*) [has_zero β] :=
(support            : finset α)
(to_fun             : α → β)
(mem_support_to_fun : ∀a, a ∈ support ↔ to_fun a ≠ 0)

infixr ` →₀ `:25 := finsupp

namespace finsupp

/-! ### Basic declarations about `finsupp` -/

section basic
variable [has_zero β]

instance : has_coe_to_fun (α →₀ β) := ⟨λ_, α → β, to_fun⟩

instance : has_zero (α →₀ β) := ⟨⟨∅, (λ_, 0), λ _, ⟨false.elim, λ H, H rfl⟩⟩⟩

@[simp] lemma zero_apply {a : α} : (0 : α →₀ β) a = 0 :=
rfl

@[simp] lemma support_zero : (0 : α →₀ β).support = ∅ :=
rfl

instance : inhabited (α →₀ β) := ⟨0⟩

@[simp] lemma mem_support_iff {f : α →₀ β} : ∀{a:α}, a ∈ f.support ↔ f a ≠ 0 :=
f.mem_support_to_fun

lemma not_mem_support_iff {f : α →₀ β} {a} : a ∉ f.support ↔ f a = 0 :=
not_iff_comm.1 mem_support_iff.symm

@[ext]
lemma ext : ∀{f g : α →₀ β}, (∀a, f a = g a) → f = g
| ⟨s, f, hf⟩ ⟨t, g, hg⟩ h :=
  begin
    have : f = g, { funext a, exact h a },
    subst this,
    have : s = t, { ext a, exact (hf a).trans (hg a).symm },
    subst this
  end

lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
⟨by rintros rfl a; refl, ext⟩

@[simp] lemma support_eq_empty {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext_iff.1 h a).1 $
  mem_support_iff.2 H, by rintro rfl; refl⟩

instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a))
  ⟨assume ⟨h₁, h₂⟩, ext $ assume a,
      if h : a ∈ f.support then h₂ a h else
        have hf : f a = 0, by rwa [mem_support_iff, not_not] at h,
        have hg : g a = 0, by rwa [h₁, mem_support_iff, not_not] at h,
        by rw [hf, hg],
    by rintro rfl; exact ⟨rfl, λ _ _, rfl⟩⟩

lemma finite_supp (f : α →₀ β) : set.finite {a | f a ≠ 0} :=
⟨fintype.of_finset f.support (λ _, mem_support_iff)⟩

lemma support_subset_iff {s : set α} {f : α →₀ β} :
  ↑f.support ⊆ s ↔ (∀a∉s, f a = 0) :=
by simp only [set.subset_def, mem_coe, mem_support_iff];
   exact forall_congr (assume a, @not_imp_comm _ _ (classical.dec _) (classical.dec _))

/-- Given `fintype α`, `equiv_fun_on_fintype` is the `equiv` between `α →₀ β` and `α → β`.
  (All functions on a finite type are finitely supported.) -/
def equiv_fun_on_fintype [fintype α] : (α →₀ β) ≃ (α → β) :=
⟨λf a, f a, λf, mk (finset.univ.filter $ λa, f a ≠ 0) f (by simp only [true_and, finset.mem_univ,
  iff_self, finset.mem_filter, finset.filter_congr_decidable, forall_true_iff]),
  begin intro f, ext a, refl end,
  begin intro f, ext a, refl end⟩

end basic

/-! ### Declarations about `single` -/

section single
variables [has_zero β] {a a' : α} {b : β}

/-- `single a b` is the finitely supported function which has
  value `b` at `a` and zero otherwise. -/
def single (a : α) (b : β) : α →₀ β :=
⟨if b = 0 then ∅ else {a}, λ a', if a = a' then b else 0, λ a', begin
  by_cases hb : b = 0; by_cases a = a';
    simp only [hb, h, if_pos, if_false, mem_singleton],
  { exact ⟨false.elim, λ H, H rfl⟩ },
  { exact ⟨false.elim, λ H, H rfl⟩ },
  { exact ⟨λ _, hb, λ _, rfl⟩ },
  { exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ }
end⟩

lemma single_apply : (single a b : α →₀ β) a' = if a = a' then b else 0 :=
rfl

@[simp] lemma single_eq_same : (single a b : α →₀ β) a = b :=
if_pos rfl

@[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ β) a' = 0 :=
if_neg h

@[simp] lemma single_zero : (single a 0 : α →₀ β) = 0 :=
ext $ assume a',
begin
  by_cases h : a = a',
  { rw [h, single_eq_same, zero_apply] },
  { rw [single_eq_of_ne h, zero_apply] }
end

lemma support_single_ne_zero (hb : b ≠ 0) : (single a b).support = {a} :=
if_neg hb

lemma support_single_subset : (single a b).support ⊆ {a} :=
show ite _ _ _ ⊆ _, by split_ifs; [exact empty_subset _, exact subset.refl _]

lemma injective_single (a : α) : function.injective (single a : β → α →₀ β) :=
assume b₁ b₂ eq,
have (single a b₁ : α →₀ β) a = (single a b₂ : α →₀ β) a, by rw eq,
by rwa [single_eq_same, single_eq_same] at this

lemma single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : β) :
  single a₁ b₁ = single a₂ b₂ ↔ ((a₁ = a₂ ∧ b₁ = b₂) ∨ (b₁ = 0 ∧ b₂ = 0)) :=
begin
  split,
  { assume eq,
    by_cases a₁ = a₂,
    { refine or.inl ⟨h, _⟩,
      rwa [h, (injective_single a₂).eq_iff] at eq },
    { rw [ext_iff] at eq,
      have h₁ := eq a₁,
      have h₂ := eq a₂,
      simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (ne.symm h)] at h₁ h₂,
      exact or.inr ⟨h₁, h₂.symm⟩ } },
  { rintros (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩),
    { refl },
    { rw [single_zero, single_zero] } }
end

lemma single_left_inj (h : b ≠ 0) :
  single a b = single a' b ↔ a = a' :=
⟨λ H, by simpa only [h, single_eq_single_iff,
  and_false, or_false, eq_self_iff_true, and_true] using H,
 λ H, by rw [H]⟩

lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
⟨λ h, by { rw ext_iff at h, simpa only [single_eq_same, zero_apply] using h a },
λ h, by rw [h, single_zero]⟩

lemma single_swap {α β : Type*} [has_zero β] (a₁ a₂ : α) (b : β) :
  (single a₁ b : α → β) a₂ = (single a₂ b : α → β) a₁ :=
by simp only [single_apply]; ac_refl

lemma unique_single [unique α] (x : α →₀ β) : x = single (default α) (x (default α)) :=
by ext i; simp only [unique.eq_default i, single_eq_same]

@[simp] lemma unique_single_eq_iff [unique α] {b' : β} :
  single a b = single a' b' ↔ b = b' :=
begin
  rw [single_eq_single_iff],
  split,
  { rintros (⟨_, rfl⟩ | ⟨rfl, rfl⟩); refl },
  { intro h, left, exact ⟨subsingleton.elim _ _, h⟩ }
end

end single

/-! ### Declarations about `on_finset` -/

section on_finset
variables [has_zero β]

/-- `on_finset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
  The function needs to be `0` outside of `s`. Use this when the set needs to be filtered anyways,
  otherwise a better set representation is often available. -/
def on_finset (s : finset α) (f : α → β) (hf : ∀a, f a ≠ 0 → a ∈ s) : α →₀ β :=
⟨s.filter (λa, f a ≠ 0), f,
  assume a, classical.by_cases
    (assume h : f a = 0, by rw mem_filter; exact ⟨and.right, λ H, (H h).elim⟩)
    (assume h : f a ≠ 0, by rw mem_filter; simp only [iff_true_intro h, hf a h, true_and])⟩

@[simp] lemma on_finset_apply {s : finset α} {f : α → β} {hf a} :
  (on_finset s f hf : α →₀ β) a = f a :=
rfl

@[simp] lemma support_on_finset_subset {s : finset α} {f : α → β} {hf} :
  (on_finset s f hf).support ⊆ s :=
filter_subset _

end on_finset

/-! ### Declarations about `map_range` -/

section map_range
variables [has_zero β₁] [has_zero β₂]

/-- The composition of `f : β₁ → β₂` and `g : α →₀ β₁` is
`map_range f hf g : α →₀ β₂`, well-defined when `f 0 = 0`. -/
def map_range (f : β₁ → β₂) (hf : f 0 = 0) (g : α →₀ β₁) : α →₀ β₂ :=
on_finset g.support (f ∘ g) $
  assume a, by rw [mem_support_iff, not_imp_not]; exact λ H, (congr_arg f H).trans hf

@[simp] lemma map_range_apply {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {a : α} :
  map_range f hf g a = f (g a) :=
rfl

@[simp] lemma map_range_zero {f : β₁ → β₂} {hf : f 0 = 0} : map_range f hf (0 : α →₀ β₁) = 0 :=
ext $ λ a, by simp only [hf, zero_apply, map_range_apply]

lemma support_map_range {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} :
  (map_range f hf g).support ⊆ g.support :=
support_on_finset_subset

@[simp] lemma map_range_single {f : β₁ → β₂} {hf : f 0 = 0} {a : α} {b : β₁} :
  map_range f hf (single a b) = single a (f b) :=
ext $ λ a', show f (ite _ _ _) = ite _ _ _, by split_ifs; [refl, exact hf]

end map_range

/-! ### Declarations about `emb_domain` -/

section emb_domain
variables [has_zero β]

/-- Given `f : α₁ ↪ α₂` and `v : α₁ →₀ β`, `emb_domain f v : α₂ →₀ β`
is the finitely supported function whose value at `f a : α₂` is `v a`.
For a `b : α₂` outside the range of `f`, it is zero. -/
def emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
begin
  refine ⟨v.support.map f, λa₂,
    if h : a₂ ∈ v.support.map f then v (v.support.choose (λa₁, f a₁ = a₂) _) else 0, _⟩,
  { rcases finset.mem_map.1 h with ⟨a, ha, rfl⟩,
    exact exists_unique.intro a ⟨ha, rfl⟩ (assume b ⟨_, hb⟩, f.inj hb) },
  { assume a₂,
    split_ifs,
    { simp only [h, true_iff, ne.def],
      rw [← not_mem_support_iff, not_not],
      apply finset.choose_mem },
    { simp only [h, ne.def, ne_self_iff_false] } }
end

lemma support_emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
  (emb_domain f v).support = v.support.map f :=
rfl

lemma emb_domain_zero (f : α₁ ↪ α₂) : (emb_domain f 0 : α₂ →₀ β) = 0 :=
rfl

lemma emb_domain_apply (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₁) :
  emb_domain f v (f a) = v a :=
begin
  change dite _ _ _ = _,
  split_ifs; rw [finset.mem_map' f] at h,
  { refine congr_arg (v : α₁ → β) (f.inj' _),
    exact finset.choose_property (λa₁, f a₁ = f a) _ _ },
  { exact (not_mem_support_iff.1 h).symm }
end

lemma emb_domain_notin_range (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
  emb_domain f v a = 0 :=
begin
  refine dif_neg (mt (assume h, _) h),
  rcases finset.mem_map.1 h with ⟨a, h, rfl⟩,
  exact set.mem_range_self a
end

lemma emb_domain_inj {f : α₁ ↪ α₂} {l₁ l₂ : α₁ →₀ β} :
  emb_domain f l₁ = emb_domain f l₂ ↔ l₁ = l₂ :=
⟨λ h, ext $ λ a, by simpa only [emb_domain_apply] using ext_iff.1 h (f a),
  λ h, by rw h⟩

lemma emb_domain_map_range
  {β₁ β₂ : Type*} [has_zero β₁] [has_zero β₂]
  (f : α₁ ↪ α₂) (g : β₁ → β₂) (p : α₁ →₀ β₁) (hg : g 0 = 0) :
  emb_domain f (map_range g hg p) = map_range g hg (emb_domain f p) :=
begin
  ext a,
  by_cases a ∈ set.range f,
  { rcases h with ⟨a', rfl⟩,
    rw [map_range_apply, emb_domain_apply, emb_domain_apply, map_range_apply] },
  { rw [map_range_apply, emb_domain_notin_range, emb_domain_notin_range, ← hg]; assumption }
end

lemma single_of_emb_domain_single
  (l : α₁ →₀ β) (f : α₁ ↪ α₂) (a : α₂) (b : β) (hb : b ≠ 0)
  (h : l.emb_domain f = single a b) :
  ∃ x, l = single x b ∧ f x = a :=
begin
  have h_map_support : finset.map f (l.support) = {a},
    by rw [←support_emb_domain, h, support_single_ne_zero hb]; refl,
  have ha : a ∈ finset.map f (l.support),
    by simp only [h_map_support, finset.mem_singleton],
  rcases finset.mem_map.1 ha with ⟨c, hc₁, hc₂⟩,
  use c,
  split,
  { ext d,
    rw [← emb_domain_apply f l, h],
    by_cases h_cases : c = d,
    { simp only [eq.symm h_cases, hc₂, single_eq_same] },
    { rw [single_apply, single_apply, if_neg, if_neg h_cases],
      by_contra hfd,
      exact h_cases (f.inj (hc₂.trans hfd)) } },
  { exact hc₂ }
end

end emb_domain

/-! ### Declarations about `zip_with` -/

section zip_with
variables [has_zero β] [has_zero β₁] [has_zero β₂]

/-- `zip_with f hf g₁ g₂` is the finitely supported function satisfying
  `zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, and it is well-defined when `f 0 0 = 0`. -/
def zip_with (f : β₁ → β₂ → β) (hf : f 0 0 = 0) (g₁ : α →₀ β₁) (g₂ : α →₀ β₂) : (α →₀ β) :=
on_finset (g₁.support ∪ g₂.support) (λa, f (g₁ a) (g₂ a)) $ λ a H,
begin
  simp only [mem_union, mem_support_iff, ne], rw [← not_and_distrib],
  rintro ⟨h₁, h₂⟩, rw [h₁, h₂] at H, exact H hf
end

@[simp] lemma zip_with_apply
  {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} {a : α} :
  zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a) :=
rfl

lemma support_zip_with {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} :
  (zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
support_on_finset_subset

end zip_with

/-! ### Declarations about `erase` -/

section erase
/-- `erase a f` is the finitely supported function equal to `f` except at `a` where it is equal to
  `0`. -/
def erase [has_zero β] (a : α) (f : α →₀ β) : α →₀ β :=
⟨f.support.erase a, (λa', if a' = a then 0 else f a'),
  assume a', by rw [mem_erase, mem_support_iff]; split_ifs;
    [exact ⟨λ H _, H.1 h, λ H, (H rfl).elim⟩,
    exact and_iff_right h]⟩

@[simp] lemma support_erase [has_zero β] {a : α} {f : α →₀ β} :
  (f.erase a).support = f.support.erase a :=
rfl

@[simp] lemma erase_same [has_zero β] {a : α} {f : α →₀ β} : (f.erase a) a = 0 :=
if_pos rfl

@[simp] lemma erase_ne [has_zero β] {a a' : α} {f : α →₀ β} (h : a' ≠ a) : (f.erase a) a' = f a' :=
if_neg h

@[simp] lemma erase_single [has_zero β] {a : α} {b : β} : (erase a (single a b)) = 0 := begin
  ext s, by_cases hs : s = a,
  { rw [hs, erase_same], refl },
  { rw [erase_ne hs], exact single_eq_of_ne (ne.symm hs) }
end

lemma erase_single_ne [has_zero β] {a a' : α} {b : β} (h : a ≠ a') : (erase a (single a' b)) = single a' b :=
begin
  ext s, by_cases hs : s = a,
  { rw [hs, erase_same, single_eq_of_ne (h.symm)] },
  { rw [erase_ne hs] }
end

end erase

/-!
### Declarations about `sum` and `prod`

In most of this section, the domain `β` is assumed to be an `add_monoid`.
-/

-- [to_additive sum] for finsupp.prod doesn't work, the equation lemmas are not generated
/-- `sum f g` is the sum of `g a (f a)` over the support of `f`. -/
def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
∑ a in f.support, g a (f a)

/-- `prod f g` is the product of `g a (f a)` over the support of `f`. -/
@[to_additive]
def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
∏ a in f.support, g a (f a)

@[to_additive]
lemma prod_fintype [fintype α] [has_zero β] [comm_monoid γ]
  (f : α →₀ β) (g : α → β → γ) (h : ∀ i, g i 0 = 1) :
  f.prod g = ∏ i, g i (f i) :=
begin
  classical,
  rw [finsupp.prod, ← fintype.prod_extend_by_one, finset.prod_congr rfl],
  intros i hi,
  split_ifs with hif hif,
  { refl },
  { rw finsupp.not_mem_support_iff at hif,
    rw [hif, h] }
end

@[to_additive]
lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ]
  {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) :
  (map_range f hf g).prod h = g.prod (λa b, h a (f b)) :=
finset.prod_subset support_map_range $ λ _ _ H,
  by rw [not_mem_support_iff.1 H, h0]

@[to_additive]
lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
  (0 : α →₀ β).prod h = 1 :=
rfl

@[to_additive]
lemma prod_comm {α' : Type*} [has_zero β] {β' : Type*} [has_zero β'] (f : α →₀ β) (g : α' →₀ β')
  [comm_monoid γ] (h : α → β → α' → β' → γ) :
  f.prod (λ x v, g.prod (λ x' v', h x v x' v')) = g.prod (λ x' v', f.prod (λ x v, h x v x' v')) :=
begin
  dsimp [finsupp.prod],
  rw finset.prod_comm,
end

@[simp, to_additive]
lemma prod_ite_eq [has_zero β] [comm_monoid γ] (f : α →₀ β) (a : α) (b : α → β → γ) :
  f.prod (λ x v, ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
by { dsimp [finsupp.prod], rw f.support.prod_ite_eq, }

/-- A restatement of `prod_ite_eq` with the equality test reversed. -/
@[simp, to_additive "A restatement of `sum_ite_eq` with the equality test reversed."]
lemma prod_ite_eq' [has_zero β] [comm_monoid γ] (f : α →₀ β) (a : α) (b : α → β → γ) :
  f.prod (λ x v, ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
by { dsimp [finsupp.prod], rw f.support.prod_ite_eq', }

@[simp] lemma prod_pow [fintype α] [comm_monoid γ] (f : α →₀ ℕ) (g : α → γ) :
  f.prod (λ a b, g a ^ b) = ∏ a, g a ^ (f a) :=
begin
  apply prod_subset (finset.subset_univ _),
  intros a _ ha,
  simp only [finsupp.not_mem_support_iff.mp ha, pow_zero]
end

section add_monoid
variables [add_monoid β]

@[to_additive]
lemma prod_single_index [comm_monoid γ] {a : α} {b : β} {h : α → β → γ} (h_zero : h a 0 = 1) :
  (single a b).prod h = h a b :=
begin
  by_cases h : b = 0,
  { simp only [h, h_zero, single_zero]; refl },
  { simp only [finsupp.prod, support_single_ne_zero h, prod_singleton, single_eq_same] }
end

instance : has_add (α →₀ β) := ⟨zip_with (+) (add_zero 0)⟩

@[simp] lemma add_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ + g₂) a = g₁ a + g₂ a :=
rfl

lemma support_add {g₁ g₂ : α →₀ β} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
support_zip_with

lemma support_add_eq {g₁ g₂ : α →₀ β} (h : disjoint g₁.support g₂.support) :
  (g₁ + g₂).support = g₁.support ∪ g₂.support :=
le_antisymm support_zip_with $ assume a ha,
(finset.mem_union.1 ha).elim
  (assume ha, have a ∉ g₂.support, from disjoint_left.1 h ha,
    by simp only [mem_support_iff, not_not] at *;
    simpa only [add_apply, this, add_zero])
  (assume ha, have a ∉ g₁.support, from disjoint_right.1 h ha,
    by simp only [mem_support_iff, not_not] at *;
    simpa only [add_apply, this, zero_add])

@[simp] lemma single_add {a : α} {b₁ b₂ : β} : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
ext $ assume a',
begin
  by_cases h : a = a',
  { rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same] },
  { rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add] }
end

instance : add_monoid (α →₀ β) :=
{ add_monoid .
  zero      := 0,
  add       := (+),
  add_assoc := assume ⟨s, f, hf⟩ ⟨t, g, hg⟩ ⟨u, h, hh⟩, ext $ assume a, add_assoc _ _ _,
  zero_add  := assume ⟨s, f, hf⟩, ext $ assume a, zero_add _,
  add_zero  := assume ⟨s, f, hf⟩, ext $ assume a, add_zero _ }

/-- Evaluation of a function `f : α →₀ β` at a point as an additive monoid homomorphism. -/
def eval_add_hom (a : α) : (α →₀ β) →+ β := ⟨λ g, g a, zero_apply, λ _ _, add_apply⟩

@[simp] lemma eval_add_hom_apply (a : α) (g : α →₀ β) : eval_add_hom a g = g a := rfl

lemma single_add_erase {a : α} {f : α →₀ β} : single a (f a) + f.erase a = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, add_zero]
else by simp only [add_apply, single_eq_of_ne h, zero_add, erase_ne (ne.symm h)]

lemma erase_add_single {a : α} {f : α →₀ β} : f.erase a + single a (f a) = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, zero_add]
else by simp only [add_apply, single_eq_of_ne h, add_zero, erase_ne (ne.symm h)]

@[simp] lemma erase_add (a : α) (f f' : α →₀ β) : erase a (f + f') = erase a f + erase a f' :=
begin
  ext s, by_cases hs : s = a,
  { rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero] },
  rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply],
end

@[elab_as_eliminator]
protected theorem induction {p : (α →₀ β) → Prop} (f : α →₀ β)
  (h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) :
  p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (single a (f a) + f.erase a), by rwa [single_add_erase] at this,
begin
  apply ha,
  { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
  { apply ih _ _,
    rw [support_erase, hf, finset.erase_insert has] }
end

lemma induction₂ {p : (α →₀ β) → Prop} (f : α →₀ β)
  (h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)) :
  p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (f.erase a + single a (f a)), by rwa [erase_add_single] at this,
begin
  apply ha,
  { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
  { apply ih _ _,
    rw [support_erase, hf, finset.erase_insert has] }
end

lemma map_range_add [add_monoid β₁] [add_monoid β₂]
  {f : β₁ → β₂} {hf : f 0 = 0} (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ β₁) :
  map_range f hf (v₁ + v₂) = map_range f hf v₁ + map_range f hf v₂ :=
ext $ λ a, by simp only [hf', add_apply, map_range_apply]

end add_monoid

section nat_sub
instance nat_sub : has_sub (α →₀ ℕ) := ⟨zip_with (λ m n, m - n) (nat.sub_zero 0)⟩

@[simp] lemma nat_sub_apply {g₁ g₂ : α →₀ ℕ} {a : α} :
  (g₁ - g₂) a = g₁ a - g₂ a :=
rfl

@[simp] lemma single_sub {a : α} {n₁ n₂ : ℕ} : single a (n₁ - n₂) = single a n₁ - single a n₂ :=
begin
  ext f,
  by_cases h : (a = f),
  { rw [h, nat_sub_apply, single_eq_same, single_eq_same, single_eq_same] },
  rw [nat_sub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h]
end

-- These next two lemmas are used in developing
-- the partial derivative on `mv_polynomial`.

lemma sub_single_one_add {a : α} {u u' : α →₀ ℕ} (h : u a ≠ 0) :
  u - single a 1 + u' = u + u' - single a 1 :=
begin
  ext b,
  rw [add_apply, nat_sub_apply, nat_sub_apply, add_apply],
  by_cases h : a = b,
  { rw [←h, single_eq_same], cases (u a), { contradiction }, { simp }, },
  { simp [h], }
end

lemma add_sub_single_one {a : α} {u u' : α →₀ ℕ} (h : u' a ≠ 0) :
  u + (u' - single a 1) = u + u' - single a 1 :=
begin
  ext b,
  rw [add_apply, nat_sub_apply, nat_sub_apply, add_apply],
  by_cases h : a = b,
  { rw [←h, single_eq_same], cases (u' a), { contradiction }, { simp }, },
  { simp [h], }
end

end nat_sub


instance [add_comm_monoid β] : add_comm_monoid (α →₀ β) :=
{ add_comm := assume ⟨s, f, _⟩ ⟨t, g, _⟩, ext $ assume a, add_comm _ _,
  .. finsupp.add_monoid }

instance [add_group β] : add_group (α →₀ β) :=
{ neg          := map_range (has_neg.neg) neg_zero,
  add_left_neg := assume ⟨s, f, _⟩, ext $ assume x, add_left_neg _,
  .. finsupp.add_monoid }

lemma single_multiset_sum [add_comm_monoid β] (s : multiset β) (a : α) :
  single a s.sum = (s.map (single a)).sum :=
multiset.induction_on s single_zero $ λ a s ih,
by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons]

lemma single_finset_sum [add_comm_monoid β] (s : finset γ) (f : γ → β) (a : α) :
  single a (∑ b in s, f b) = ∑ b in s, single a (f b) :=
begin
  transitivity,
  apply single_multiset_sum,
  rw [multiset.map_map],
  refl
end

lemma single_sum [has_zero γ] [add_comm_monoid β] (s : δ →₀ γ) (f : δ → γ → β) (a : α) :
  single a (s.sum f) = s.sum (λd c, single a (f d c)) :=
single_finset_sum _ _ _


@[to_additive]
lemma prod_neg_index [add_group β] [comm_monoid γ]
  {g : α →₀ β} {h : α → β → γ} (h0 : ∀a, h a 0 = 1) :
  (-g).prod h = g.prod (λa b, h a (- b)) :=
prod_map_range_index h0

@[simp] lemma neg_apply [add_group β] {g : α →₀ β} {a : α} : (- g) a = - g a :=
rfl

@[simp] lemma sub_apply [add_group β] {g₁ g₂ : α →₀ β} {a : α} : (g₁ - g₂) a = g₁ a - g₂ a :=
rfl

@[simp] lemma support_neg [add_group β] {f : α →₀ β} : support (-f) = support f :=
finset.subset.antisymm
  support_map_range
  (calc support f = support (- (- f)) : congr_arg support (neg_neg _).symm
     ... ⊆ support (- f) : support_map_range)

instance [add_comm_group β] : add_comm_group (α →₀ β) :=
{ add_comm := add_comm, ..finsupp.add_group }

@[simp] lemma sum_apply [has_zero β₁] [add_comm_monoid β]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β} {a₂ : α} :
  (f.sum g) a₂ = f.sum (λa₁ b, g a₁ b a₂) :=
(eval_add_hom a₂ : (α →₀ β) →+ _).map_sum _ _

lemma support_sum [has_zero β₁] [add_comm_monoid β]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → (α →₀ β)} :
  (f.sum g).support ⊆ f.support.bind (λa, (g a (f a)).support) :=
have ∀a₁ : α, f.sum (λ (a : α₁) (b : β₁), (g a b) a₁) ≠ 0 →
    (∃ (a : α₁), f a ≠ 0 ∧ ¬ (g a (f a)) a₁ = 0),
  from assume a₁ h,
  let ⟨a, ha, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
  ⟨a, mem_support_iff.mp ha, ne⟩,
by simpa only [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply, exists_prop]
  using this

@[simp] lemma sum_zero [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β} :
  f.sum (λa b, (0 : γ)) = 0 :=
finset.sum_const_zero

@[simp] lemma sum_add  [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β}
  {h₁ h₂ : α → β → γ} :
  f.sum (λa b, h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂ :=
finset.sum_add_distrib

@[simp] lemma sum_neg [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
  {h : α → β → γ} : f.sum (λa b, - h a b) = - f.sum h :=
f.support.sum_hom (@has_neg.neg γ _)

@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
  {h₁ h₂ : α → β → γ} :
  f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl

@[simp] lemma sum_single [add_comm_monoid β] (f : α →₀ β) :
  f.sum single = f :=
have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =
    ∑ a' in {a}, ite (a' = a) (f a') 0,
begin
  intro a,
  by_cases h : a ∈ f.support,
  { have : ({a} : finset α) ⊆ f.support,
      { simpa only [finset.subset_iff, mem_singleton, forall_eq] },
    refine (finset.sum_subset this (λ _ _ H, _)).symm,
    exact if_neg (mt mem_singleton.2 H) },
  { transitivity (∑ a in f.support, (0 : β)),
    { refine (finset.sum_congr rfl $ λ a' ha', if_neg _),
      rintro rfl, exact h ha' },
    { rw [sum_const_zero, sum_singleton, if_pos rfl, not_mem_support_iff.1 h] } }
end,
ext $ assume a, by simp only [sum_apply, single_apply, this, sum_singleton, if_pos]

@[to_additive]
lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f + g).prod h = f.prod h * g.prod h :=
have f_eq : ∏ a in f.support ∪ g.support, h a (f a) = f.prod h,
  from (finset.prod_subset (finset.subset_union_left _ _) $
    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
have g_eq : ∏ a in f.support ∪ g.support, h a (g a) = g.prod h,
  from (finset.prod_subset (finset.subset_union_right _ _) $
    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
calc ∏ a in (f + g).support, h a ((f + g) a) =
      ∏ a in f.support ∪ g.support, h a ((f + g) a) :
    finset.prod_subset support_add $
      by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]
  ... = (∏ a in f.support ∪ g.support, h a (f a)) *
      (∏ a in f.support ∪ g.support, h a (g a)) :
    by simp only [add_apply, h_add, finset.prod_mul_distrib]
  ... = _ : by rw [f_eq, g_eq]

lemma sum_sub_index [add_comm_group β] [add_comm_group γ] {f g : α →₀ β}
  {h : α → β → γ} (h_sub : ∀a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) :
  (f - g).sum h = f.sum h - g.sum h :=
have h_zero : ∀a, h a 0 = 0,
  from assume a,
  have h a (0 - 0) = h a 0 - h a 0, from h_sub a 0 0,
  by simpa only [sub_self] using this,
have h_neg : ∀a b, h a (- b) = - h a b,
  from assume a b,
  have h a (0 - b) = h a 0 - h a b, from h_sub a 0 b,
  by simpa only [h_zero, zero_sub] using this,
have h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂,
  from assume a b₁ b₂,
  have h a (b₁ - (- b₂)) = h a b₁ - h a (- b₂), from h_sub a b₁ (-b₂),
  by simpa only [h_neg, sub_neg_eq_add] using this,
calc (f - g).sum h = (f + - g).sum h : rfl
  ... = f.sum h + - g.sum h : by simp only [sum_add_index h_zero h_add, sum_neg_index h_zero,
                                   h_neg, sum_neg]
  ... = f.sum h - g.sum h : rfl

@[to_additive]
lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ]
  {s : finset ι} {g : ι → α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  ∏ i in s, (g i).prod h = (∑ i in s, g i).prod h :=
finset.induction_on s rfl $ λ a s has ih,
by rw [prod_insert has, ih, sum_insert has, prod_add_index h_zero h_add]

@[to_additive]
lemma prod_sum_index
  [add_comm_monoid β₁] [add_comm_monoid β] [comm_monoid γ]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f.sum g).prod h = f.prod (λa b, (g a b).prod h) :=
(prod_finset_sum_index h_zero h_add).symm

lemma multiset_sum_sum_index
  [add_comm_monoid β] [add_comm_monoid γ]
  (f : multiset (α →₀ β)) (h : α → β → γ)
  (h₀ : ∀a, h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
  (f.sum.sum h) = (f.map $ λg:α →₀ β, g.sum h).sum :=
multiset.induction_on f rfl $ assume a s ih,
by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index h₀ h₁, ih]

lemma multiset_map_sum [has_zero β] {f : α →₀ β} {m : γ → δ} {h : α → β → multiset γ} :
  multiset.map m (f.sum h) = f.sum (λa b, (h a b).map m) :=
(f.support.sum_hom _).symm

lemma multiset_sum_sum [has_zero β] [add_comm_monoid γ] {f : α →₀ β} {h : α → β → multiset γ} :
  multiset.sum (f.sum h) = f.sum (λa b, multiset.sum (h a b)) :=
(f.support.sum_hom multiset.sum).symm

section map_range
variables
  [add_comm_monoid β₁] [add_comm_monoid β₂]
  (f : β₁ → β₂) [hf : is_add_monoid_hom f]

instance is_add_monoid_hom_map_range :
  is_add_monoid_hom (map_range f hf.map_zero : (α →₀ β₁) → (α →₀ β₂)) :=
{ map_zero := map_range_zero, map_add := λ a b, map_range_add hf.map_add _ _ }

lemma map_range_multiset_sum (m : multiset (α →₀ β₁)) :
  map_range f hf.map_zero m.sum = (m.map $ λx, map_range f hf.map_zero x).sum :=
(m.sum_hom (map_range f hf.map_zero)).symm

lemma map_range_finset_sum {ι : Type*} (s : finset ι) (g : ι → (α →₀ β₁))  :
  map_range f hf.map_zero (∑ x in s, g x) = ∑ x in s, map_range f hf.map_zero (g x) :=
by rw [finset.sum.equations._eqn_1, map_range_multiset_sum, multiset.map_map]; refl

end map_range

/-! ### Declarations about `map_domain` -/

section map_domain
variables [add_comm_monoid β] {v v₁ v₂ : α →₀ β}

/-- Given `f : α₁ → α₂` and `v : α₁ →₀ β`, `map_domain f v : α₂ →₀ β`
  is the finitely supported function whose value at `a : α₂` is the sum
  of `v x` over all `x` such that `f x = a`. -/
def map_domain (f : α₁ → α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
v.sum $ λa, single (f a)

lemma map_domain_apply {f : α₁ → α₂} (hf : function.injective f) (x : α₁ →₀ β) (a : α₁) :
  map_domain f x (f a) = x a :=
begin
  rw [map_domain, sum_apply, sum, finset.sum_eq_single a, single_eq_same],
  { assume b _ hba, exact single_eq_of_ne (hf.ne hba) },
  { simp only [(∉), (≠), not_not, mem_support_iff],
    assume h,
    rw [h, single_zero],
    refl }
end

lemma map_domain_notin_range {f : α₁ → α₂} (x : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
  map_domain f x a = 0 :=
begin
  rw [map_domain, sum_apply, sum],
  exact finset.sum_eq_zero
    (assume a' h', single_eq_of_ne $ assume eq, h $ eq ▸ set.mem_range_self _)
end

lemma map_domain_id : map_domain id v = v :=
sum_single _

lemma map_domain_comp {f : α → α₁} {g : α₁ → α₂} :
  map_domain (g ∘ f) v = map_domain g (map_domain f v) :=
begin
  refine ((sum_sum_index _ _).trans _).symm,
  { intros, exact single_zero },
  { intros, exact single_add },
  refine sum_congr rfl (λ _ _, sum_single_index _),
  { exact single_zero }
end

lemma map_domain_single {f : α → α₁} {a : α} {b : β} : map_domain f (single a b) = single (f a) b :=
sum_single_index single_zero

@[simp] lemma map_domain_zero {f : α → α₂} : map_domain f 0 = (0 : α₂ →₀ β) :=
sum_zero_index

lemma map_domain_congr {f g : α → α₂} (h : ∀x∈v.support, f x = g x) :
  v.map_domain f = v.map_domain g :=
finset.sum_congr rfl $ λ _ H, by simp only [h _ H]

lemma map_domain_add {f : α → α₂} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
sum_add_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_finset_sum {f : α → α₂} {s : finset ι} {v : ι → α →₀ β} :
  map_domain f (∑ i in s, v i) = ∑ i in s, map_domain f (v i) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_sum [has_zero β₁] {f : α → α₂} {s : α →₀ β₁} {v : α → β₁ → α →₀ β} :
  map_domain f (s.sum v) = s.sum (λa b, map_domain f (v a b)) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_support {f : α → α₂} {s : α →₀ β} :
  (s.map_domain f).support ⊆ s.support.image f :=
finset.subset.trans support_sum $
  finset.subset.trans (finset.bind_mono $ assume a ha, support_single_subset) $
  by rw [finset.bind_singleton]; exact subset.refl _

@[to_additive]
lemma prod_map_domain_index [comm_monoid γ] {f : α → α₂} {s : α →₀ β}
  {h : α₂ → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (s.map_domain f).prod h = s.prod (λa b, h (f a) b) :=
(prod_sum_index h_zero h_add).trans $ prod_congr rfl $ λ _ _, prod_single_index (h_zero _)

lemma emb_domain_eq_map_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
  emb_domain f v = map_domain f v :=
begin
  ext a,
  by_cases a ∈ set.range f,
  { rcases h with ⟨a, rfl⟩,
    rw [map_domain_apply f.inj, emb_domain_apply] },
  { rw [map_domain_notin_range, emb_domain_notin_range]; assumption }
end

lemma injective_map_domain {f : α₁ → α₂} (hf : function.injective f) :
  function.injective (map_domain f : (α₁ →₀ β) → (α₂ →₀ β)) :=
begin
  assume v₁ v₂ eq, ext a,
  have : map_domain f v₁ (f a) = map_domain f v₂ (f a), { rw eq },
  rwa [map_domain_apply hf, map_domain_apply hf] at this,
end

end map_domain

/-! ### Declarations about `comap_domain` -/

section comap_domain

/-- Given `f : α₁ → α₂`, `l : α₂ →₀ γ` and a proof `hf` that `f` is injective on
the preimage of `l.support`, `comap_domain f l hf` is the finitely supported function
from `α₁` to `γ` given by composing `l` with `f`. -/
def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' ↑l.support)) : α₁ →₀ γ :=
{ support := l.support.preimage hf,
  to_fun := (λ a, l (f a)),
  mem_support_to_fun :=
    begin
      intros a,
      simp only [finset.mem_def.symm, finset.mem_preimage],
      exact l.mem_support_to_fun (f a),
    end }

@[simp]
lemma comap_domain_apply {α₁ α₂ γ : Type*} [has_zero γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' ↑l.support)) (a : α₁) :
  comap_domain f l hf a = l (f a) :=
rfl

lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ β) (g : α₂ → β → γ)
  (hf : set.bij_on f (f ⁻¹' ↑l.support) ↑l.support) :
  (comap_domain f l hf.inj_on).sum (g ∘ f) = l.sum g :=
begin
  simp [sum],
  simp [comap_domain, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))]
end

lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' ↑l.support) ↑l.support) :
   comap_domain f l hf.inj_on = 0 → l = 0 :=
begin
  rw [← support_eq_empty, ← support_eq_empty, comap_domain],
  simp only [finset.ext_iff, finset.not_mem_empty, iff_false, mem_preimage],
  assume h a ha,
  cases hf.2.2 ha with b hb,
  exact h b (hb.2.symm ▸ ha)
end

lemma map_domain_comap_domain {α₁ α₂ γ : Type*} [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ)
  (hf : function.injective f) (hl : ↑l.support ⊆ set.range f):
  map_domain f (comap_domain f l (hf.inj_on _)) = l :=
begin
  ext a,
  by_cases h_cases: a ∈ set.range f,
  { rcases set.mem_range.1 h_cases with ⟨b, hb⟩,
    rw [hb.symm, map_domain_apply hf, comap_domain_apply] },
  { rw map_domain_notin_range _ _ h_cases,
    by_contra h_contr,
    apply h_cases (hl $ finset.mem_coe.2 $ mem_support_iff.2 $ λ h, h_contr h.symm) }
end

end comap_domain

/-! ### Declarations about `filter` -/

section filter
section has_zero
variables [has_zero β] (p : α → Prop) (f : α →₀ β)

/-- `filter p f` is the function which is `f a` if `p a` is true and 0 otherwise. -/
def filter (p : α → Prop) (f : α →₀ β) : α →₀ β :=
on_finset f.support (λa, if p a then f a else 0) $ λ a H,
mem_support_iff.2 $ λ h, by rw [h, if_t_t] at H; exact H rfl

@[simp] lemma filter_apply_pos {a : α} (h : p a) : f.filter p a = f a :=
if_pos h

@[simp] lemma filter_apply_neg {a : α} (h : ¬ p a) : f.filter p a = 0 :=
if_neg h

@[simp] lemma support_filter : (f.filter p).support = f.support.filter p :=
finset.ext $ assume a, if H : p a
then by simp only [mem_support_iff, filter_apply_pos _ _ H, mem_filter, H, and_true]
else by simp only [mem_support_iff, filter_apply_neg _ _ H, mem_filter, H, and_false, ne.def,
  ne_self_iff_false]

lemma filter_zero : (0 : α →₀ β).filter p = 0 :=
by rw [← support_eq_empty, support_filter, support_zero, finset.filter_empty]

@[simp] lemma filter_single_of_pos
  {a : α} {b : β} (h : p a) : (single a b).filter p = single a b :=
ext $ λ x, begin
  by_cases h' : p x,
  { simp only [h', filter_apply_pos] },
  { simp only [h', filter_apply_neg, not_false_iff],
    rw single_eq_of_ne, rintro rfl, exact h' h }
end

@[simp] lemma filter_single_of_neg
  {a : α} {b : β} (h : ¬ p a) : (single a b).filter p = 0 :=
ext $ λ x, begin
  by_cases h' : p x,
  { simp only [h', filter_apply_pos, zero_apply], rw single_eq_of_ne, rintro rfl, exact h h' },
  { simp only [h', finsupp.zero_apply, not_false_iff, filter_apply_neg] }
end

end has_zero

lemma filter_pos_add_filter_neg [add_monoid β] (f : α →₀ β) (p : α → Prop) :
  f.filter p + f.filter (λa, ¬ p a) = f :=
ext $ assume a, if H : p a
then by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_not, add_zero]
else by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_false_iff, zero_add]

end filter

/-! ### Declarations about `frange` -/

section frange
variables [has_zero β]

/-- `frange f` is the image of `f` on the support of `f`. -/
def frange (f : α →₀ β) : finset β := finset.image f f.support

theorem mem_frange {f : α →₀ β} {y : β} :
  y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y :=
finset.mem_image.trans
⟨λ ⟨x, hx1, hx2⟩, ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩,
λ ⟨hy, x, hx⟩, ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

theorem zero_not_mem_frange {f : α →₀ β} : (0:β) ∉ f.frange :=
λ H, (mem_frange.1 H).1 rfl

theorem frange_single {x : α} {y : β} : frange (single x y) ⊆ {y} :=
λ r hr, let ⟨t, ht1, ht2⟩ := mem_frange.1 hr in ht2 ▸
  (by rw single_apply at ht2 ⊢; split_ifs at ht2 ⊢; [exact finset.mem_singleton_self _, cc])

end frange

/-! ### Declarations about `subtype_domain` -/

section subtype_domain

variables {α' : Type*} [has_zero δ] {p : α → Prop}

section zero
variables [has_zero β] {v v' : α' →₀ β}

/-- `subtype_domain p f` is the restriction of the finitely supported function
  `f` to the subtype `p`. -/
def subtype_domain (p : α → Prop) (f : α →₀ β) : (subtype p →₀ β) :=
⟨f.support.subtype p, f ∘ subtype.val, λ a, by simp only [mem_subtype, mem_support_iff]⟩

@[simp] lemma support_subtype_domain {f : α →₀ β} :
  (subtype_domain p f).support = f.support.subtype p :=
rfl

@[simp] lemma subtype_domain_apply {a : subtype p} {v : α →₀ β} :
  (subtype_domain p v) a = v (a.val) :=
rfl

@[simp] lemma subtype_domain_zero : subtype_domain p (0 : α →₀ β) = 0 :=
rfl

@[to_additive]
lemma prod_subtype_domain_index [comm_monoid γ] {v : α →₀ β}
  {h : α → β → γ} (hp : ∀x∈v.support, p x) :
  (v.subtype_domain p).prod (λa b, h a.1 b) = v.prod h :=
prod_bij (λp _, p.val)
  (λ _, mem_subtype.1)
  (λ _ _, rfl)
  (λ _ _ _ _, subtype.eq)
  (λ b hb, ⟨⟨b, hp b hb⟩, mem_subtype.2 hb, rfl⟩)

end zero

section monoid
variables [add_monoid β] {v v' : α' →₀ β}

@[simp] lemma subtype_domain_add {v v' : α →₀ β} :
  (v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
ext $ λ _, rfl

instance subtype_domain.is_add_monoid_hom :
  is_add_monoid_hom (subtype_domain p : (α →₀ β) → subtype p →₀ β) :=
{ map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }

@[simp] lemma filter_add {v v' : α →₀ β} :
  (v + v').filter p = v.filter p + v'.filter p :=
ext $ λ a, begin
  by_cases p a,
  { simp only [h, filter_apply_pos, add_apply] },
  { simp only [h, add_zero, add_apply, not_false_iff, filter_apply_neg] }
end

instance filter.is_add_monoid_hom (p : α → Prop) :
  is_add_monoid_hom (filter p : (α →₀ β) → (α →₀ β)) :=
{ map_zero := filter_zero p, map_add := λ x y, filter_add }

end monoid

section comm_monoid
variables [add_comm_monoid β]

lemma subtype_domain_sum {s : finset γ} {h : γ → α →₀ β} :
  (∑ c in s, h c).subtype_domain p = ∑ c in s, (h c).subtype_domain p :=
eq.symm (s.sum_hom _)

lemma subtype_domain_finsupp_sum {s : γ →₀ δ} {h : γ → δ → α →₀ β} :
  (s.sum h).subtype_domain p = s.sum (λc d, (h c d).subtype_domain p) :=
subtype_domain_sum

lemma filter_sum (s : finset γ) (f : γ → α →₀ β) :
  (∑ a in s, f a).filter p = ∑ a in s, filter p (f a) :=
(s.sum_hom (filter p)).symm

end comm_monoid

section group
variables [add_group β] {v v' : α' →₀ β}

@[simp] lemma subtype_domain_neg {v : α →₀ β} :
  (- v).subtype_domain p = - v.subtype_domain p :=
ext $ λ _, rfl

@[simp] lemma subtype_domain_sub {v v' : α →₀ β} :
  (v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
ext $ λ _, rfl

end group

end subtype_domain

/-! ### Declarations relating `finsupp` to `multiset` -/

section multiset

/-- Given `f : α →₀ ℕ`, `f.to_multiset` is the multiset with multiplicities given by the values of
`f` on the elements of `α`. -/
def to_multiset (f : α →₀ ℕ) : multiset α :=
f.sum (λa n, n •ℕ {a})

lemma to_multiset_zero : (0 : α →₀ ℕ).to_multiset = 0 :=
rfl

lemma to_multiset_add (m n : α →₀ ℕ) :
  (m + n).to_multiset = m.to_multiset + n.to_multiset :=
sum_add_index (assume a, zero_nsmul _) (assume a b₁ b₂, add_nsmul _ _ _)

lemma to_multiset_single (a : α) (n : ℕ) : to_multiset (single a n) = n •ℕ {a} :=
by rw [to_multiset, sum_single_index]; apply zero_nsmul

instance is_add_monoid_hom.to_multiset : is_add_monoid_hom (to_multiset : _ → multiset α) :=
{ map_zero := to_multiset_zero, map_add := to_multiset_add }

lemma card_to_multiset (f : α →₀ ℕ) : f.to_multiset.card = f.sum (λa, id) :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.card_zero, sum_zero_index] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.card_add, ih, sum_add_index, to_multiset_single,
      sum_single_index, multiset.card_smul, multiset.singleton_eq_singleton,
      multiset.card_singleton, mul_one]; intros; refl }
end

lemma to_multiset_map (f : α →₀ ℕ) (g : α → β) :
  f.to_multiset.map g = (f.map_domain g).to_multiset :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.map_zero, map_domain_zero, to_multiset_zero] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.map_add, ih, map_domain_add, map_domain_single,
      to_multiset_single, to_multiset_add, to_multiset_single,
      is_add_monoid_hom.map_nsmul (multiset.map g)],
    refl }
end

lemma prod_to_multiset [comm_monoid α] (f : α →₀ ℕ) :
  f.to_multiset.prod = f.prod (λa n, a ^ n) :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.prod_zero, finsupp.prod_zero_index] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, finsupp.prod_add_index,
      finsupp.prod_single_index, multiset.prod_smul, multiset.singleton_eq_singleton,
      multiset.prod_singleton],
    { exact pow_zero a },
    { exact pow_zero },
    { exact pow_add  } }
end

lemma to_finset_to_multiset (f : α →₀ ℕ) : f.to_multiset.to_finset = f.support :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.to_finset_zero, support_zero] },
  { assume a n f ha hn ih,
    rw [to_multiset_add, multiset.to_finset_add, ih, to_multiset_single, support_add_eq,
      support_single_ne_zero hn, multiset.to_finset_nsmul _ _ hn,
      multiset.singleton_eq_singleton, multiset.to_finset_cons, multiset.to_finset_zero],
    refl,
    refine disjoint.mono_left support_single_subset _,
    rwa [finset.singleton_disjoint] }
end

@[simp] lemma count_to_multiset (f : α →₀ ℕ) (a : α) :
  f.to_multiset.count a = f a :=
calc f.to_multiset.count a = f.sum (λx n, (n •ℕ {x} : multiset α).count a) :
    (f.support.sum_hom $ multiset.count a).symm
  ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
  ... = f.sum (λx n, n * (x :: 0 : multiset α).count a) : rfl
  ... = f a * (a :: 0 : multiset α).count a : sum_eq_single _
    (λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])
    (λ H, by simp only [not_mem_support_iff.1 H, zero_mul])
  ... = f a : by simp only [multiset.count_singleton, mul_one]

/-- Given `m : multiset α`, `of_multiset m` is the finitely supported function from `α` to `ℕ`
given by the multiplicities of the elements of `α` in `m`. -/
def of_multiset (m : multiset α) : α →₀ ℕ :=
on_finset m.to_finset (λa, m.count a) $ λ a H, multiset.mem_to_finset.2 $
by_contradiction (mt multiset.count_eq_zero.2 H)

@[simp] lemma of_multiset_apply (m : multiset α) (a : α) :
  of_multiset m a = m.count a :=
rfl

/-- `equiv_multiset` defines an `equiv` between finitely supported functions
from `α` to `ℕ` and multisets on `α`. -/
def equiv_multiset : (α →₀ ℕ) ≃ (multiset α) :=
⟨ to_multiset, of_multiset,
assume f, finsupp.ext $ λ a, by rw [of_multiset_apply, count_to_multiset],
assume m, multiset.ext.2 $ λ a, by rw [count_to_multiset, of_multiset_apply] ⟩

lemma mem_support_multiset_sum [add_comm_monoid β]
  {s : multiset (α →₀ β)} (a : α) :
  a ∈ s.sum.support → ∃f∈s, a ∈ (f : α →₀ β).support :=
multiset.induction_on s false.elim
  begin
    assume f s ih ha,
    by_cases a ∈ f.support,
    { exact ⟨f, multiset.mem_cons_self _ _, h⟩ },
    { simp only [multiset.sum_cons, mem_support_iff, add_apply,
        not_mem_support_iff.1 h, zero_add] at ha,
      rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩,
      exact ⟨f', multiset.mem_cons_of_mem h₀, h₁⟩ }
  end

lemma mem_support_finset_sum [add_comm_monoid β]
  {s : finset γ} {h : γ → α →₀ β} (a : α) (ha : a ∈ (∑ c in s, h c).support) : ∃c∈s, a ∈ (h c).support :=
let ⟨f, hf, hfa⟩ := mem_support_multiset_sum a ha in
let ⟨c, hc, eq⟩ := multiset.mem_map.1 hf in
⟨c, hc, eq.symm ▸ hfa⟩

lemma mem_support_single [has_zero β] (a a' : α) (b : β) :
  a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0 :=
⟨λ H : (a ∈ ite _ _ _), if h : b = 0
  then by rw if_pos h at H; exact H.elim
  else ⟨by rw if_neg h at H; exact mem_singleton.1 H, h⟩,
λ ⟨h1, h2⟩, show a ∈ ite _ _ _, by rw [if_neg h2]; exact mem_singleton.2 h1⟩

end multiset

/-! ### Declarations about `curry` and `uncurry` -/

section curry_uncurry

/-- Given a finitely supported function `f` from a product type `α × β` to `γ`,
`curry f` is the "curried" finitely supported function from `α` to the type of
finitely supported functions from `β` to `γ`. -/
protected def curry [add_comm_monoid γ]
  (f : (α × β) →₀ γ) : α →₀ (β →₀ γ) :=
f.sum $ λp c, single p.1 (single p.2 c)

lemma sum_curry_index
  [add_comm_monoid γ] [add_comm_monoid δ]
  (f : (α × β) →₀ γ) (g : α → β → γ → δ)
  (hg₀ : ∀ a b, g a b 0 = 0) (hg₁ : ∀a b c₀ c₁, g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
  f.curry.sum (λa f, f.sum (g a)) = f.sum (λp c, g p.1 p.2 c) :=
begin
  rw [finsupp.curry],
  transitivity,
  { exact sum_sum_index (assume a, sum_zero_index)
      (assume a b₀ b₁, sum_add_index (assume a, hg₀ _ _) (assume c d₀ d₁, hg₁ _ _ _ _)) },
  congr, funext p c,
  transitivity,
  { exact sum_single_index sum_zero_index },
  exact sum_single_index (hg₀ _ _)
end

/-- Given a finitely supported function `f` from `α` to the type of
finitely supported functions from `β` to `γ`,
`uncurry f` is the "uncurried" finitely supported function from `α × β` to `γ`. -/
protected def uncurry [add_comm_monoid γ] (f : α →₀ (β →₀ γ)) : (α × β) →₀ γ :=
f.sum $ λa g, g.sum $ λb c, single (a, b) c

/-- `finsupp_prod_equiv` defines the `equiv` between `((α × β) →₀ γ)` and `(α →₀ (β →₀ γ))` given by
currying and uncurrying. -/
def finsupp_prod_equiv [add_comm_monoid γ] : ((α × β) →₀ γ) ≃ (α →₀ (β →₀ γ)) :=
by refine ⟨finsupp.curry, finsupp.uncurry, λ f, _, λ f, _⟩; simp only [
  finsupp.curry, finsupp.uncurry, sum_sum_index, sum_zero_index, sum_add_index,
  sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff,
  forall_3_true_iff, prod.mk.eta, (single_sum _ _ _).symm, sum_single]

lemma filter_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) (p : α₁ → Prop) :
  (f.filter (λa:α₁×α₂, p a.1)).curry = f.curry.filter p :=
begin
  rw [finsupp.curry, finsupp.curry, finsupp.sum, finsupp.sum,
    @filter_sum _ (α₂ →₀ β) _ p _ f.support _],
  rw [support_filter, sum_filter],
  refine finset.sum_congr rfl _,
  rintros ⟨a₁, a₂⟩ ha,
  dsimp only,
  split_ifs,
  { rw [filter_apply_pos, filter_single_of_pos]; exact h },
  { rwa [filter_single_of_neg] }
end

lemma support_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) :
  f.curry.support ⊆ f.support.image prod.fst :=
begin
  rw ← finset.bind_singleton,
  refine finset.subset.trans support_sum _,
  refine finset.bind_mono (assume a _, support_single_subset)
end

end curry_uncurry

section
variables [group γ] [mul_action γ α] [add_comm_monoid β]

/--
Scalar multiplication by a group element g,
given by precomposition with the action of g⁻¹ on the domain.
-/
def comap_has_scalar : has_scalar γ (α →₀ β) :=
{ smul := λ g f, f.comap_domain (λ a, g⁻¹ • a)
  (λ a a' m m' h, by simpa [←mul_smul] using (congr_arg (λ a, g • a) h)) }

local attribute [instance] comap_has_scalar

/--
Scalar multiplication by a group element,
given by precomposition with the action of g⁻¹ on the domain,
is multiplicative in g.
-/
def comap_mul_action : mul_action γ (α →₀ β) :=
{ one_smul := λ f, by { ext, dsimp [(•)], simp, },
  mul_smul := λ g g' f, by { ext, dsimp [(•)], simp [mul_smul], }, }

local attribute [instance] comap_mul_action

/--
Scalar multiplication by a group element,
given by precomposition with the action of g⁻¹ on the domain,
is additive in the second argument.
-/
def comap_distrib_mul_action :
  distrib_mul_action γ (α →₀ β) :=
{ smul_zero := λ g, by { ext, dsimp [(•)], simp, },
  smul_add := λ g f f', by { ext, dsimp [(•)], simp, }, }

/--
Scalar multiplication by a group element on finitely supported functions on a group,
given by precomposition with the action of g⁻¹. -/
def comap_distrib_mul_action_self :
  distrib_mul_action γ (γ →₀ β) :=
@finsupp.comap_distrib_mul_action γ β γ _ (mul_action.regular γ) _

@[simp]
lemma comap_smul_single (g : γ) (a : α) (b : β) :
  g • single a b = single (g • a) b :=
begin
  ext a',
  dsimp [(•)],
  by_cases h : g • a = a',
  { subst h, simp [←mul_smul], },
  { simp [single_eq_of_ne h], rw [single_eq_of_ne],
    rintro rfl, simpa [←mul_smul] using h, }
end

@[simp]
lemma comap_smul_apply (g : γ) (f : α →₀ β) (a : α) :
  (g • f) a = f (g⁻¹ • a) := rfl

end

section
instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : has_scalar γ (α →₀ β) :=
⟨λa v, v.map_range ((•) a) (smul_zero _)⟩

variables (α β)

@[simp] lemma smul_apply' {R:semiring γ} [add_comm_monoid β] [semimodule γ β]
  {a : α} {b : γ} {v : α →₀ β} : (b • v) a = b • (v a) :=
rfl

instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : semimodule γ (α →₀ β) :=
{ smul      := (•),
  smul_add  := λ a x y, ext $ λ _, smul_add _ _ _,
  add_smul  := λ a x y, ext $ λ _, add_smul _ _ _,
  one_smul  := λ x, ext $ λ _, one_smul _ _,
  mul_smul  := λ r s x, ext $ λ _, mul_smul _ _ _,
  zero_smul := λ x, ext $ λ _, zero_smul _ _,
  smul_zero := λ x, ext $ λ _, smul_zero _ }

variables {α β} (γ)

/-- Evaluation at point as a linear map. This version assumes that the codomain is a semimodule
over some semiring. See also `leval`. -/
def leval' [semiring γ] [add_comm_monoid β] [semimodule γ β] (a : α) :
  (α →₀ β) →ₗ[γ] β :=
⟨λ g, g a, λ _ _, add_apply, λ _ _, rfl⟩

@[simp] lemma coe_leval' [semiring γ] [add_comm_monoid β] [semimodule γ β] (a : α) (g : α →₀ β) :
  leval' γ a g = g a :=
rfl

variable {γ}

/-- Evaluation at point as a linear map. This version assumes that the codomain is a semiring. -/
def leval [semiring β] (a : α) : (α →₀ β) →ₗ[β] β := leval' β a

@[simp] lemma coe_leval [semiring β] (a : α) (g : α →₀ β) : leval a g = g a := rfl

lemma support_smul {R:semiring γ} [add_comm_monoid β] [semimodule γ β] {b : γ} {g : α →₀ β} :
  (b • g).support ⊆ g.support :=
λ a, by simp only [smul_apply', mem_support_iff, ne.def]; exact mt (λ h, h.symm ▸ smul_zero _)

section
variables {α' : Type*} [has_zero δ] {p : α → Prop}

@[simp] lemma filter_smul {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
  {b : γ} {v : α →₀ β} : (b • v).filter p = b • v.filter p :=
ext $ λ a, begin
  by_cases p a,
  { simp only [h, smul_apply', filter_apply_pos] },
  { simp only [h, smul_apply', not_false_iff, filter_apply_neg, smul_zero] }
end

end

lemma map_domain_smul {α'} {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
   {f : α → α'} (b : γ) (v : α →₀ β) : map_domain f (b • v) = b • map_domain f v :=
begin
  change map_domain f (map_range _ _ _) = map_range _ _ _,
  apply finsupp.induction v, { simp only [map_domain_zero, map_range_zero] },
  intros a b v' hv₁ hv₂ IH,
  rw [map_range_add, map_domain_add, IH, map_domain_add, map_range_add,
    map_range_single, map_domain_single, map_domain_single, map_range_single];
  apply smul_add
end

@[simp] lemma smul_single {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
  (c : γ) (a : α) (b : β) : c • finsupp.single a b = finsupp.single a (c • b) :=
ext $ λ a', by by_cases a = a';
  [{ subst h, simp only [smul_apply', single_eq_same] },
   simp only [h, smul_apply', ne.def, not_false_iff, single_eq_of_ne, smul_zero]]

@[simp] lemma smul_single' {R : semiring γ}
  (c : γ) (a : α) (b : γ) : c • finsupp.single a b = finsupp.single a (c * b) :=
smul_single _ _ _

end

@[simp] lemma smul_apply [semiring β] {a : α} {b : β} {v : α →₀ β} :
  (b • v) a = b • (v a) :=
rfl

lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ}
  (h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
finsupp.sum_map_range_index h0

section
variables [semiring β] [semiring γ]

lemma sum_mul (b : γ) (s : α →₀ β) {f : α → β → γ} :
  (s.sum f) * b = s.sum (λ a c, (f a (s a)) * b) :=
by simp only [finsupp.sum, finset.sum_mul]

lemma mul_sum (b : γ) (s : α →₀ β) {f : α → β → γ} :
  b * (s.sum f) = s.sum (λ a c, b * (f a (s a))) :=
by simp only [finsupp.sum, finset.mul_sum]

protected lemma eq_zero_of_zero_eq_one
  (zero_eq_one : (0 : β) = 1) (l : α →₀ β) : l = 0 :=
by ext i; simp only [eq_zero_of_zero_eq_one β zero_eq_one (l i), finsupp.zero_apply]

end

/-- Given an `add_comm_monoid β` and `s : set α`, `restrict_support_equiv s β` is the `equiv`
between the subtype of finitely supported functions with support contained in `s` and
the type of finitely supported functions from `s`. -/
def restrict_support_equiv (s : set α) (β : Type*) [add_comm_monoid β] :
  {f : α →₀ β // ↑f.support ⊆ s } ≃ (s →₀ β):=
begin
  refine ⟨λf, subtype_domain (λx, x ∈ s) f.1, λ f, ⟨f.map_domain subtype.val, _⟩, _, _⟩,
  { refine set.subset.trans (finset.coe_subset.2 map_domain_support) _,
    rw [finset.coe_image, set.image_subset_iff],
    exact assume x hx, x.2 },
  { rintros ⟨f, hf⟩,
    apply subtype.eq,
    ext a,
    dsimp only,
    refine classical.by_cases (assume h : a ∈ set.range (subtype.val : s → α), _) (assume h, _),
    { rcases h with ⟨x, rfl⟩,
      rw [map_domain_apply subtype.val_injective, subtype_domain_apply] },
    { convert map_domain_notin_range _ _ h,
      rw [← not_mem_support_iff],
      refine mt _ h,
      exact assume ha, ⟨⟨a, hf ha⟩, rfl⟩ } },
  { assume f,
    ext ⟨a, ha⟩,
    dsimp only,
    rw [subtype_domain_apply, map_domain_apply subtype.val_injective] }
end

/-- Given `add_comm_monoid β` and `e : α₁ ≃ α₂`, `dom_congr e` is the corresponding `equiv` between
`α₁ →₀ β` and `α₂ →₀ β`. -/
protected def dom_congr [add_comm_monoid β] (e : α₁ ≃ α₂) : (α₁ →₀ β) ≃ (α₂ →₀ β) :=
⟨map_domain e, map_domain e.symm,
  begin
    assume v,
    simp only [map_domain_comp.symm, (∘), equiv.symm_apply_apply],
    exact map_domain_id
  end,
  begin
    assume v,
    simp only [map_domain_comp.symm, (∘), equiv.apply_symm_apply],
    exact map_domain_id
  end⟩

/-! ### Declarations about sigma types -/

section sigma

variables {αs : ι → Type*} [has_zero β] (l : (Σ i, αs i) →₀ β)

/-- Given `l`, a finitely supported function from the sigma type `Σ (i : ι), αs i` to `β` and
an index element `i : ι`, `split l i` is the `i`th component of `l`,
a finitely supported function from `as i` to `β`. -/
def split (i : ι) : αs i →₀ β :=
l.comap_domain (sigma.mk i) (λ x1 x2 _ _ hx, heq_iff_eq.1 (sigma.mk.inj hx).2)

lemma split_apply (i : ι) (x : αs i) : split l i x = l ⟨i, x⟩ :=
begin
  dunfold split,
  rw comap_domain_apply
end

/-- Given `l`, a finitely supported function from the sigma type `Σ (i : ι), αs i` to `β`,
`split_support l` is the finset of indices in `ι` that appear in the support of `l`. -/
def split_support : finset ι := l.support.image sigma.fst

lemma mem_split_support_iff_nonzero (i : ι) :
  i ∈ split_support l ↔ split l i ≠ 0 :=
begin
  rw [split_support, mem_image, ne.def, ← support_eq_empty, ← ne.def,
    ← finset.nonempty_iff_ne_empty, split, comap_domain, finset.nonempty],
  simp only [exists_prop, finset.mem_preimage, exists_and_distrib_right, exists_eq_right,
    mem_support_iff, sigma.exists, ne.def]
end

/-- Given `l`, a finitely supported function from the sigma type `Σ i, αs i` to `β` and
an `ι`-indexed family `g` of functions from `(αs i →₀ β)` to `γ`, `split_comp` defines a
finitely supported function from the index type `ι` to `γ` given by composing `g i` with
`split l i`. -/
def split_comp [has_zero γ] (g : Π i, (αs i →₀ β) → γ)
  (hg : ∀ i x, x = 0 ↔ g i x = 0) : ι →₀ γ :=
{ support := split_support l,
  to_fun := λ i, g i (split l i),
  mem_support_to_fun :=
  begin
    intros i,
    rw [mem_split_support_iff_nonzero, not_iff_not, hg],
  end }

lemma sigma_support : l.support = l.split_support.sigma (λ i, (l.split i).support) :=
by simp only [finset.ext_iff, split_support, split, comap_domain, mem_image,
  mem_preimage, sigma.forall, mem_sigma]; tauto

lemma sigma_sum [add_comm_monoid γ] (f : (Σ (i : ι), αs i) → β → γ) :
  l.sum f = ∑ i in split_support l, (split l i).sum (λ (a : αs i) b, f ⟨i, a⟩ b) :=
by simp only [sum, sigma_support, sum_sigma, split_apply]

end sigma

end finsupp

/-! ### Declarations relating `multiset` to `finsupp` -/

namespace multiset

/-- Given a multiset `s`, `s.to_finsupp` returns the finitely supported function on `ℕ` given by
the multiplicities of the elements of `s`. -/
def to_finsupp (s : multiset α) : α →₀ ℕ :=
{ support := s.to_finset,
  to_fun := λ a, s.count a,
  mem_support_to_fun := λ a,
  begin
    rw mem_to_finset,
    convert not_iff_not_of_iff (count_eq_zero.symm),
    rw not_not
  end }

@[simp] lemma to_finsupp_support (s : multiset α) :
  s.to_finsupp.support = s.to_finset :=
rfl

@[simp] lemma to_finsupp_apply (s : multiset α) (a : α) :
  s.to_finsupp a = s.count a :=
rfl

@[simp] lemma to_finsupp_zero :
  to_finsupp (0 : multiset α) = 0 :=
finsupp.ext $ λ a, count_zero a

@[simp] lemma to_finsupp_add (s t : multiset α) :
  to_finsupp (s + t) = to_finsupp s + to_finsupp t :=
finsupp.ext $ λ a, count_add a s t

lemma to_finsupp_singleton (a : α) :
  to_finsupp {a} = finsupp.single a 1 :=
finsupp.ext $ λ b,
if h : a = b then by rw [to_finsupp_apply, finsupp.single_apply, h, if_pos rfl,
  singleton_eq_singleton, count_singleton] else
begin
  rw [to_finsupp_apply, finsupp.single_apply, if_neg h, count_eq_zero,
      singleton_eq_singleton, mem_singleton],
  rintro rfl, exact h rfl
end

namespace to_finsupp

instance : is_add_monoid_hom (to_finsupp : multiset α → α →₀ ℕ) :=
{ map_zero := to_finsupp_zero,
  map_add  := to_finsupp_add }

end to_finsupp

@[simp] lemma to_finsupp_to_multiset (s : multiset α) :
  s.to_finsupp.to_multiset = s :=
ext.2 $ λ a, by rw [finsupp.count_to_multiset, to_finsupp_apply]

end multiset

/-! ### Declarations about order(ed) instances on `finsupp` -/

namespace finsupp
variables {σ : Type*}

instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ le := λ f g, ∀ s, f s ≤ g s,
  le_refl := λ f s, le_refl _,
  le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }

instance [partial_order α] [has_zero α] : partial_order (σ →₀ α) :=
{ le_antisymm := λ f g hfg hgf, ext $ λ s, le_antisymm (hfg s) (hgf s),
  .. finsupp.preorder }

instance [ordered_cancel_add_comm_monoid α] :
  add_left_cancel_semigroup (σ →₀ α) :=
{ add_left_cancel := λ a b c h, ext $ λ s,
  by { rw ext_iff at h, exact add_left_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_add_comm_monoid α] :
  add_right_cancel_semigroup (σ →₀ α) :=
{ add_right_cancel := λ a b c h, ext $ λ s,
  by { rw ext_iff at h, exact add_right_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_add_comm_monoid α] :
  ordered_cancel_add_comm_monoid (σ →₀ α) :=
{ add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
  le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
  .. finsupp.add_comm_monoid, .. finsupp.partial_order,
  .. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }

lemma le_iff [canonically_ordered_add_monoid α] (f g : σ →₀ α) :
  f ≤ g ↔ ∀ s ∈ f.support, f s ≤ g s :=
⟨λ h s hs, h s,
λ h s, if H : s ∈ f.support then h s H else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩

@[simp] lemma add_eq_zero_iff [canonically_ordered_add_monoid α] (f g : σ →₀ α) :
  f + g = 0 ↔ f = 0 ∧ g = 0 :=
begin
  split,
  { assume h,
    split,
    all_goals
    { ext s,
      suffices H : f s + g s = 0,
      { rw add_eq_zero_iff at H, cases H, assumption },
      show (f + g) s = 0,
      rw h, refl } },
  { rintro ⟨rfl, rfl⟩, rw add_zero }
end

attribute [simp] to_multiset_zero to_multiset_add

@[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :
  f.to_multiset.to_finsupp = f :=
ext $ λ s, by rw [multiset.to_finsupp_apply, count_to_multiset]

lemma to_multiset_strict_mono : strict_mono (@to_multiset σ) :=
λ m n h,
begin
  rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
  split,
  { rw multiset.le_iff_count, intro s, erw [count_to_multiset m s, count_to_multiset], exact h₁ s },
  { intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H,
    simpa only [to_multiset_to_finsupp] using H }
end

lemma sum_id_lt_of_lt (m n : σ →₀ ℕ) (h : m < n) :
  m.sum (λ _, id) < n.sum (λ _, id) :=
begin
  rw [← card_to_multiset, ← card_to_multiset],
  apply multiset.card_lt_of_lt,
  exact to_multiset_strict_mono h
end

variable (σ)

/-- The order on `σ →₀ ℕ` is well-founded.-/
lemma lt_wf : well_founded (@has_lt.lt (σ →₀ ℕ) _) :=
subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf

instance decidable_le : decidable_rel (@has_le.le (σ →₀ ℕ) _) :=
λ m n, by rw le_iff; apply_instance

variable {σ}

/-- The `finsupp` counterpart of `multiset.antidiagonal`: the antidiagonal of
`s : σ →₀ ℕ` consists of all pairs `(t₁, t₂) : (σ →₀ ℕ) × (σ →₀ ℕ)` such that `t₁ + t₂ = s`.
The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs. -/
def antidiagonal (f : σ →₀ ℕ) : ((σ →₀ ℕ) × (σ →₀ ℕ)) →₀ ℕ :=
(f.to_multiset.antidiagonal.map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finsupp

lemma mem_antidiagonal_support {f : σ →₀ ℕ} {p : (σ →₀ ℕ) × (σ →₀ ℕ)} :
  p ∈ (antidiagonal f).support ↔ p.1 + p.2 = f :=
begin
  erw [multiset.mem_to_finset, multiset.mem_map],
  split,
  { rintros ⟨⟨a, b⟩, h, rfl⟩,
    rw multiset.mem_antidiagonal at h,
    simpa only [to_multiset_to_finsupp, multiset.to_finsupp_add]
      using congr_arg multiset.to_finsupp h},
  { intro h,
    refine ⟨⟨p.1.to_multiset, p.2.to_multiset⟩, _, _⟩,
    { simpa only [multiset.mem_antidiagonal, to_multiset_add]
        using congr_arg to_multiset h},
    { rw [prod.map, to_multiset_to_finsupp, to_multiset_to_finsupp, prod.mk.eta] } }
end

@[simp] lemma antidiagonal_zero : antidiagonal (0 : σ →₀ ℕ) = single (0,0) 1 :=
by rw [← multiset.to_finsupp_singleton]; refl

lemma swap_mem_antidiagonal_support {n : σ →₀ ℕ} {f} (hf : f ∈ (antidiagonal n).support) :
  f.swap ∈ (antidiagonal n).support :=
by simpa only [mem_antidiagonal_support, add_comm, prod.swap] using hf

/-- Let `n : σ →₀ ℕ` be a finitely supported function.
The set of `m : σ →₀ ℕ` that are coordinatewise less than or equal to `n`,
is a finite set. -/
lemma finite_le_nat (n : σ →₀ ℕ) : set.finite {m | m ≤ n} :=
begin
  let I := {i // i ∈ n.support},
  let k : ℕ := ∑ i in n.support, n i,
  let f : (σ →₀ ℕ) → (I → fin (k + 1)) := λ m i, m i,
  have hf : ∀ m ≤ n, ∀ i, (f m i : ℕ) = m i,
  { intros m hm i,
    apply fin.coe_coe_of_lt,
    calc m i ≤ n i   : hm i
         ... < k + 1 : nat.lt_succ_iff.mpr (single_le_sum (λ _ _, nat.zero_le _) i.2) },
  have f_im : set.finite (f '' {m | m ≤ n}) := set.finite.of_fintype _,
  suffices f_inj : set.inj_on f {m | m ≤ n},
  { exact set.finite_of_finite_image f_inj f_im },
  intros m₁ m₂ h₁ h₂ h,
  ext i,
  by_cases hi : i ∈ n.support,
  { replace h := congr_fun h ⟨i, hi⟩,
    rwa [fin.ext_iff, ← fin.coe_eq_val, ← fin.coe_eq_val, hf m₁ h₁, hf m₂ h₂] at h },
  { rw not_mem_support_iff at hi,
    specialize h₁ i,
    specialize h₂ i,
    rw [hi, nat.le_zero_iff] at h₁ h₂,
    rw [h₁, h₂] }
end

/-- Let `n : σ →₀ ℕ` be a finitely supported function.
The set of `m : σ →₀ ℕ` that are coordinatewise less than or equal to `n`,
but not equal to `n` everywhere, is a finite set. -/
lemma finite_lt_nat (n : σ →₀ ℕ) : set.finite {m | m < n} :=
set.finite_subset (finite_le_nat n) $ λ m, le_of_lt

end finsupp
